FDL - Step of Proof: fib

Step of Proof: fib_wf

11,40

Inference at *
Iof proof for Lemma fib wf:

. fib(n)

by ((((D 0)

CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n

C)) (first_tok :t) inil_term)))

)

CollapseTHEN (((OnVar `n' CompNatInd)

CollapseTHENA (

C(Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 1000:n)) (first_tok :t) inil_term)))

))

C1:

C1: 1. n :

C1: 2.

n1:

. (n1 < n)

(fib(n1)

)

C1:

fib(n)

Definitions , , False, A, A B, i j , P Q, t T, x:A. B(x)

Lemmas le wf, ge wf, nat properties, nat wf

Definitions	, , False, A, A B, i j , P Q, t T, x:A. B(x)
Lemmas	le wf, ge wf, nat properties, nat wf